Kripke frame - .｡oO(さっちゃんですよヾ(〃l

Kripke frame

Kripke 意味論 (Kripke semantics)。可能世界意味論

Kripke frame とは$ Wを集合として、二項關係$ R\subseteq W\times Wとの組$ (W,R)を言ふ

Kripke model とは Kripke frame に、集合$ Wの要素と命題との以下の條件を滿たす二項關係$ \Vdashを足した組$ (W,R,\Vdash)である

$ w\Vdash\neg A\iff w\cancel\Vdash A.

$ w\Vdash A\to B\iff w\cancel\Vdash A\lor w\Vdash B.

$ w\Vdash\square A\iff\forall u_{\in W}(wRu\land u\Vdash A).

命題文$ Aが Kripke model$ M=(W,R,\Vdash)に於いて妥當であるとは$ \forall w_{\in W}(w\Vdash A)である事を言ひ、$ M\vDash Aと書く

命題文$ Aが Kripke frame$ F上の任意の Kripke model で妥當であれば、$ Aは$ F上で妥當であると言ひ、$ F\vDash Aと書く

命題文$ Aが Kripke frame の類 (class)$ {\bf C}_Fに屬する任意の Kripke model 上で妥當であれば、$ Aが$ \bf C_Fで妥當であると言ひ、$ {\bf C_F}\vDash Aと書く

集合$ Wの要素は「世界」より「場所」と呼ぶのが穩當ではないか

bounded morphism (p-morphism (pseudo-epimorphism))

Kripke frame$ (W,R)と$ (W',R')が有り、寫像$ f:W\to W'は以下を滿たす時、$ (W,R)から$ (W',R')への bounded morphism と呼ぶ

$ \forall u,w_{\in W}(uRw\to f(u)R'f(w))關係を保存する

$ \forall u_{\in W},w'_{\in W'}(f(u)R'w'\to\exist w_{\in W}(uRw\land f(w)=w'))關係を考慮した全射

Kripke model 閒の bounded morphism は更に、全ての命題變數$ pに就いて$ w\Vdash p\iff f(w)\Vdash'pを滿たす

雙模倣 (bisimulation)

Kripke frame$ (W,R)と$ (W',R')が在る時、二項關係$ B\subseteq W\times W'が雙模倣であるとは以下の zig-zag property が滿たされる事を言ふ

$ uBu'\land uRw\to\exist w'_{\in W'}(wBw'\land u'R'w').

$ uBu'\land u'R'w'\to\exist w_{\in W}(wBw'\land uRw).

Kripke model 閒の雙模倣は更に、全ての命題變數$ pに就いて$ wBw'\to (w\Vdash p\iff w'\Vdash'p)を滿たす

反射律$ wRwと推移律$ uRv\land vRw\to uRwを滿たす Kripke frame は圈である

反射律は公理 T$ \square A\to A

推移律は公理 4$ \square A\to\square\square A

IL frame とも呼び$ (W,\le)と書く

Kripke frame は集合$ Wからその冪集合$ 2^Wへの自己函手$ {\cal P}:W\to 2^Wの$ \cal P-餘代數である

Kripke frame は bounded morphism を射として圈を成し、この圈は$ \cal P-餘代數の圈$ {\bf Coalg}({\cal P})と圈同型である

擴張

general frame$ (W,R_{\subseteq W\times W},A_{\subseteq 2^W})

Routley-Meyer frame$ (W,R_{\subseteq W\times W\times W},^*_{:W\to W},0_{\in W})

近傍 frame$ (W,N_{:W\to2^{2^W}})